FDL - Nuprl Definition : alle-between1

Nuprl Definition : alle-between1

0,22

[e1,e2).P(e) ==

e:E. e1

(e <loc e2)

P(e)

clarification:

alle-between1(es;e1;e2;e.P(e)) ==

e:es-E(es). es-le(es;e1;e)

es-locl(es; e; e2)

P(e)

Definitions e[e1,e2).P(e), x:A. B(x), E, e e' , P Q, (e <loc e')

FDL editor aliases alle-between1

Definitions	e[e1,e2).P(e), x:A. B(x), E, e e' , P Q, (e <loc e')
FDL editor aliases	alle-between1